Nuprl Lemma : s-insert_wf
11,40
postcript
pdf
T
:Type. subtype_rel(
T
;
)
(
x
:
T
,
L
:(
T
List). s-insert(
x
;
L
)
(
T
List))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
i
<z
j
,
if
b
then
t
else
f
fi
,
(
i
=
j
)
,
s-insert(
x
;
l
)
,
P
Q
Lemmas
eq
int
wf
,
ifthenelse
wf
,
lt
int
wf
origin